package at.tasat.solver;

import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import at.tasat.cnf.Clause;
import at.tasat.cnf.Literal;

public class VariableOccurences implements Cloneable {

	private final int variableId;
	private HashSet<Clause> positiveOccurences;
	private HashSet<Clause> negativeOccurences;

	public VariableOccurences(int variableId) {
		this(variableId, new HashSet<Clause>(), new HashSet<Clause>());
	}

	private VariableOccurences(int variableId, HashSet<Clause> positiveOccurences, HashSet<Clause> negativeOccurences) {
		this.variableId = variableId;
		this.positiveOccurences = positiveOccurences;
		this.negativeOccurences = negativeOccurences;
	}

	public int getVariableId() {
		return variableId;
	}

	public int getNumberOfOccurences() {
		return negativeOccurences.size() + positiveOccurences.size();
	}

	public boolean getDominantPhase() {
		return positiveOccurences.size() >= negativeOccurences.size();
	}

	public boolean isPurePositive() {
		return negativeOccurences.size() == 0;
	}

	public boolean isPureNegative() {
		return positiveOccurences.size() == 0;
	}

	public Iterator<Clause> getPositiveOccurences() {
		return positiveOccurences.iterator();
	}

	public Iterator<Clause> getNegativeOccurences() {
		return negativeOccurences.iterator();
	}

	public Iterator<Clause> getOccurences(boolean phase) {
		return phase ? getPositiveOccurences() : getNegativeOccurences();
	}

	public Set<Clause> removeOccurences(boolean phase) {
		Set<Clause> removedClauses;
		if (phase) {
			removedClauses = positiveOccurences;
			positiveOccurences = new HashSet<Clause>();
		} else {
			removedClauses = negativeOccurences;
			negativeOccurences = new HashSet<Clause>();
		}
		return removedClauses;
	}

	public void addClauses(Collection<Clause> clauses) {
		for (Clause clause : clauses) {
			addClause(clause);
		}
	}

	public void addClause(Clause clause) {
		int literal = clause.getLiteralOfVariable(variableId);
		if (literal != 0) {
			if (Literal.getPhase(literal)) {
				positiveOccurences.add(clause);
			} else {
				negativeOccurences.add(clause);
			}
		}
	}

	public void removeClauses(Collection<Clause> clauses) {
		negativeOccurences.removeAll(clauses);
		positiveOccurences.removeAll(clauses);
	}

	@SuppressWarnings("unchecked")
	public VariableOccurences clone() {
		return new VariableOccurences(variableId, 
				(HashSet<Clause>) positiveOccurences.clone(), 
				(HashSet<Clause>) negativeOccurences.clone());
	}
}
